Social bots are computer programs that act like human users on social media platforms. Social bot detection is a rapidly growing field dominated by machine learning approaches. In this paper, we propose a complementary method to machine learning by exploring bot detection as a model checking problem. We introduce Temporal Network Logic (TNL) which we use to specify social networks where agents can post and follow each other. Using this logic, we formalize different types of social bot behavior with formulas (...) that are satisfied in a model of a network with bots. We also consider an extension of the logic where we explore the expressive power of including elements from hybrid logic in our framework. We give model checking algorithms for TNL and its hybrid extension, and show that the complexity of the former is in p and the latter in pspace. (shrink)

Formal learning theory formalizes the process of inferring a general result from examples, as in the case of inferring grammars from sentences when learning a language. In this work, we develop a general framework—the supervised learning game—to investigate the interaction between Teacher and Learner. In particular, our proposal highlights several interesting features of the agents: on the one hand, Learner may make mistakes in the learning process, and she may also ignore the potential relation between different hypotheses; on the other (...) hand, Teacher is able to correct Learner’s mistakes, eliminate potential mistakes and point out the facts ignored by Learner. To reason about strategies in this game, we develop a modal logic of supervised learning and study its properties. Broadly, this work takes a small step towards studying the interaction between graph games, logics and formal learning theory. (shrink)

Software-controlled bots, also called social bots, are computer programs that act like human users on social media platforms. Recent work on detection of social bots is dominated by machine learning approaches. In this paper we explore bot detection as a model checking problem. We introduce Temporal Network Logic which we use to specify social networks where agents can post and follow each other. In this logic we formalize different types of social bot behavior. These are formulas that are satisfied in (...) a model of a network with bots. We provide a simple algorithm to extract a logical model from a real-life social network. We show that we can reduce TNL to a fragment of linear temporal logic with past and use this to establish the computational efficiency of model checking for social bot detection. (shrink)